Filteration for de Morgan style modal logic
論理式の定義として以下を採用する．
1. 命題変項として$ p,q,\dotsがあるとき，対応してその補$ \bar{p},\bar{q},\dotsがあるとする．命題変項とその補は論理式である．
2. $ \top,\botは論理式である．
3. 論理式$ A,Bに対して$ A \land B,A\lor B,\Box A,\Diamond Aは論理式である．
4. 否定$ \lnotは以下のように定義する．（片側はだけ．要は双対）
$ \lnot p \equiv \bar{p}，$ \lnot \bar{p} \equiv p
$ \lnot (A \land B) \equiv \lnot A \lor \lnot B
$ \lnot \top \equiv \bot
$ \lnot \Box A \equiv \Diamond \lnot A
5. $ A \to B \equiv \lnot A \lor Bとする．
意味論，証明論はいつものように定義する．問題となるのは濾過法の部分．
Recall
論理式$ Aの部分論理式$ \mathrm{Sub}(A)は通常通り定める．
$ \Sigmaが部分論理式で閉じているとは，任意の$ A \in \Sigmaに対して$ \mathrm{Sub}(A) \sube \Sigmaとなることである．
以下$ \Sigmaは補を含めて論理式で閉じているとする．
Filteration
$ M := \lang W,R,\Vdash\rangの$ \Sigmaによる濾過モデル$ M^f_\Sigma := \lang W^f, R^f, \Vdash^f \rang
$ W^f := W / \mathord{\sim_\Sigma}とする．
$ R^f：$ x R^f yは次を満たす
1. $ x R y \implies \lbrack x \rbrack R^f \lbrack y \rbrack
2. $ \lbrack x \rbrack R^f \lbrack y \rbrackのとき
任意の$ \Box A \in \Sigmaに対して$ M,x \vDash \Box A \implies M, y \vDash A
$ \Vdash^f
$ p \in \Sigmaなら$ \lbrack x \rbrack \Vdash^f p \iff x \Vdash p
Thm. Filteration Theorem
$ M := \lang W, R, \Vdash \rangとし，$ \Sigmaは部分論理式に閉じた論理式の集合とする．$ A \in \Sigmaなら
$ M,x \vDash A \iff M^f_\Sigma, \lbrack x\rbrack \vDash A
proof of FT, Part 1
$ A \equiv p,\bar{p}, \Box B, \Diamond Bを見る．
$ A \equiv p
定義より$ p \in \Sigmaなら$ \lbrack x \rbrack \Vdash^f p \iff x \Vdash pだったから良い．
$ A \equiv \bar{p}
$ \lbrack x \rbrack \vDash \bar{p} \iff \lbrack x \rbrack \nVdash^f pだった．
このとき$ \Vdash^fの定義より$ x \nVdash pが言える…ように見える．しかし次の問題がある
$ \lbrack x \rbrack \Vdash^f \bar{p} \iff \lbrack x \rbrack \nVdash^f p